\begin{tabbing}
approx\_sm(${\it es}$; ${\it In}$; ${\it Out}$; ${\it Cmd}$; ${\it isupdate}$; ${\it Rsp}$; ${\it Delta}$; $Q$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$\=${\it expl}$:E(${\it Out}$)$\rightarrow$(\{$e$:E(${\it In}$)$\mid$ $\uparrow$(${\it isupdate}$(${\it In}$($e$)))\}  List)\+
\\[0ex]((\=$\forall$$e$:E(${\it Out}$).\+
\\[0ex]($\forall$${\it e'}$:E(${\it In}$). (${\it e'}$ $\in$ ${\it expl}$($e$)) $\Rightarrow$ ${\it e'}$ c$\leq$ $e$)
\\[0ex]\& (($\neg$is{-}query(${\it In}$;${\it isupdate}$;$e$)) $\Rightarrow$ ($\neg$($\uparrow$null(${\it expl}$($e$))))))
\-\\[0ex]\& ($\forall$$e_{1}$, $e_{2}$:E(${\it Out}$). ${\it expl}$($e_{1}$) $\leq$ ${\it expl}$($e_{2}$) $\vee$ ${\it expl}$($e_{2}$) $\leq$ ${\it expl}$($e_{1}$))
\\[0ex]\& (\=$\forall$$e$:E(${\it Out}$).\+
\\[0ex](is{-}query(${\it In}$;${\it isupdate}$;$e$) $\Rightarrow$ (${\it Out}$($e$) = $Q$(${\it In}$(${\it expl}$($e$)),${\it In}$($e$))))
\\[0ex]\& (($\neg$is{-}query(${\it In}$;${\it isupdate}$;$e$)) $\Rightarrow$ (${\it Out}$($e$) = ${\it Delta}$(${\it In}$(${\it expl}$($e$)))))))
\-\-
\end{tabbing}